FDL - Nuprl Lemma : bnot_of_le_int

Nuprl Lemma : bnot_of_le_int

i, j:

. (

i

z j) = j <z i

Up bool 1, bool 1

Definitions t T, x:A. B(x), i z j, P Q, P & Q, P Q, P Q

Lemmas bnot bnot elim, lt int wf, bool wf